v:. 0 < v  0 < (1/v) 

latex

Definitions	(i = j), ff, b, i <z j, tt, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.1, , gset, goset, t.2, , x f y, p  q, a < b, if b then t else f fi , a <p b, a < b, r * s, qeq(r;s), b, r < s, P & Q, T, P  Q, P  Q, True, (r/s), A, t  T, , P  Q, x:A. B(x), P  Q, False, S  T
Lemmas	qless transitivity, qless-minus, qmul inv, qmul com, qmul comm qrng, qmul one qrng, qmul wf, true wf, squash wf, qinv wf, qless irreflexivity, qle weakening eq qorder, qless transitivity 2 qorder, rationals wf, qless wf, int inc rationals, qdiv wf, qmul-positive, assert-qeq, qeq wf2, assert wf, not functionality wrt iff